/* Franco, 26/02/2010.
   A simple test to check perfect recall verification using the
   following hand-coded model (for a single agent):
   S = {s0,...,s7}
   Rt = { (s0,s1), (s0,s2), (s0,s3), (s1,s4), (s2,s4), (s3,s5),
   (s4,s0), (s5,s6), (s6,s0) }
   Ri equivalence classes: { {s0}, {s1,s2,s3}, {s4,s6}, {s5} } 
   Evaluation: L(s0) = a; L(s1)=L(s2)=L(s3)=b; L(s4)=c; L(s5)=d, L(s6)=c}

   The idea is that K(b) is true in the equiv. class of s1 and K(c) is
   true in the equiv class of s4, but with perfect recall K(b) is true
   in s1 and s2 only, and K(c) in s4 only.

*/

#include "cuddObj.hh"
#include "utilities.hh"
#include "formula.hh"
#include <cmath>
// #include <ctime>



int main(int argc, char* argv[]) {

  // Initial declarations, valid for all models
  Cudd *bddmgr = new Cudd(0,0);
  map<string, BDD*> *evaluation = new map<string,BDD*>();
  BDD *Rt = new BDD();
  BDD *Ri = new BDD();
  vector<BDD *> *EC = new vector<BDD *>();
  int depth = 0; // the max depth of a computation (see reachable
		 // states)


  Cudd_ReorderingType REORDERING = CUDD_REORDER_GROUP_SIFT_CONV;
  Cudd_AutodynEnable(bddmgr->getManager(), REORDERING);

  // Model-specific code
  int states_count = atoi(argv[1]); // (7 states = 3 variables)
  BDDvector *v = new BDDvector(states_count,bddmgr); 
  BDDvector *pv = new BDDvector(states_count,bddmgr); 
  
  for (int i = 0; i < states_count; i++) {
    (*v)[i] = bddmgr->bddVar(i);
    (*pv)[i] = bddmgr->bddVar(states_count + i);
  }  

  build_test_model(bddmgr,v,pv,Rt,Ri,evaluation);  
  // End of model specific code



  // Compute reachable (assuming state 0 is the initial state)
  BDD *reach = new BDD();
  reach = compute_reachable_states(stateid_to_BDD(0,v,bddmgr),Rt,v,
				   pv,bddmgr,depth);
  // Compute equivalence classes
  EC = compute_EC(Ri,v,pv,bddmgr,reach);


  // MODEL CHECKING PART
  Formula* atom_c = new Formula("c");
  Formula* f = new Formula(30,atom_c);
  f->set_depth(3);
  f->set_name("AgentName");

  cout << f->to_string() << endl;

  BDD *result = new BDD(*f->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,
                                          reach));
  result->print(2,2);



  Formula* atom_a = new Formula("a");
  Formula* atom_b = new Formula("b");
  Formula* atom_d = new Formula("d");


  cout << "Now playing with K1" << endl;
  Formula* k1a = new Formula(32,atom_a);
  k1a->set_depth(1);
  k1a->set_EC(EC);
  result = (k1a->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,
			       reach));
  result->print(2,2);


  Formula* k1b = new Formula(32,atom_b);
  k1b->set_depth(1);
  k1b->set_EC(EC);
  result = (k1b->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,
			       reach));
  result->print(2,2);


  Formula* k1d = new Formula(32,atom_d);
  k1d->set_depth(1);
  k1d->set_EC(EC);
  result = (k1d->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,
			       reach));
  result->print(2,2);  





  cout << "Now playing with KPR" << endl;
  Formula* kpra = new Formula(31,atom_a);
  kpra->set_model_depth(depth);
  kpra->set_EC(EC);
  result = (kpra->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,
			       reach));
  result->print(2,2);


  Formula* kprb = new Formula(31,atom_b);
  kprb->set_model_depth(depth);
  kprb->set_EC(EC);
  result = (kprb->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,
			       reach));
  result->print(2,2);


  Formula* kprd = new Formula(31,atom_d);
  kprd->set_model_depth(depth);
  kprd->set_EC(EC);
  result = (kprd->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,
			       reach));
  result->print(2,2);  




  time_t endtime;
  time ( &endtime );
  cout << "Job completed on: " <<  ctime (&endtime);
  cout << "Have a great day and drive safely!" << endl;

}
